Nuprl Lemma : not_over_exists
12,41
postcript
pdf
T
:Type,
Q
:(
T
). (
(
x
:
T
.
Q
(
x
)))
(
x
:
T
.
Q
(
x
))
latex
ProofTree
Definitions
t
T
,
P
Q
,
P
Q
,
P
&
Q
,
x
(
s
)
,
x
:
A
.
B
(
x
)
,
P
Q
,
,
x
:
A
.
B
(
x
)
,
A
,
False
Lemmas
not
wf
origin
T:Type, Q:(T
). (
(
x:T. Q(x))) 
(x:T. Q(x))
T:Type, Q:(T). ((x:T. Q(x))) (x:T. Q(x))
T Q Qx:A. B(x) Qx:A. B(x)A